Termination Proof Script

• Consider the SCC {11}. The usable rules are {3,5,6}. By taking the AF π with π(F) = 1 and π(n__s) = π(p) = π(s) = [ ] together with the lexicographic path order with precedence s ≻ n__s and s ≻ p ≻ 0 ≻ n__0, the rules in {3,5,6,11} are strictly decreasing.


• Consider the SCC {14,16}. There are no usable rules. By taking the AF π with π(ACTIVATE) = π(n__f) = 1 together with the lexicographic path order with empty precedence, rule 14 is weakly decreasing and rule 16 is strictly decreasing. There is one new SCC.
  • Consider the SCC {14}. By taking the AF π with π(ACTIVATE) = 1 together with the lexicographic path order with empty precedence, rule 14 is strictly decreasing.